rel\_implies($T$; $R_{1}$; $R_{2}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$, $y$:$T$. ($x$ $R_{1}$ $y$) $\Rightarrow$ ($x$ $R_{2}$ $y$)